D:Dsys. d-empty()  D 

latex

Definitions	t  T, f(a), x:A. B(x), MsgA, Id, Type, x:AB(x), , M1  M2, M(i), D1  D2, d-empty(), Dsys
Lemmas	Id wf, msga wf, ma-empty-sub